package com.itesm.sistemasinteligentes.sat;
import java.util.HashMap;
import java.util.Map;

public abstract class SATSolver implements Runnable {

	protected int[][] clauses;
	protected HashMap<Integer, Boolean> variables;
	protected int maxFlips;
	protected long startTime;
	protected int flipsRequired;
	protected int flipsInLastTry;
	protected int triesRequired;
	protected long endTime;
	protected int maxTries;
	protected int maxThreads;
	
	public volatile boolean stopThread = false;	
	public volatile boolean solverFinished = false;
	
	protected volatile boolean solutionFound = false;

	public SATSolver(int[][] clauses, int maxFlips, int maxTries) {
		this.clauses = clauses;
		this.maxFlips = maxFlips;
		this.variables = extractVariables();
		this.maxTries = maxTries;
	}

	protected abstract boolean solveImplementation();

	/**
	 * This method try to resolve the SAT problem. When finished will return
	 * true if the problem was solved or false if the problem could not be
	 * solved. If the problem was successfully solved you can call report method
	 * to get the details of the execution.
	 * 
	 * @return true if the problem was solved or false if the problem could not
	 *         be solved
	 */
	public final boolean solve() {
		startTime = System.currentTimeMillis();
		boolean result = solveImplementation();
		endTime = System.currentTimeMillis();
		return result;
	}

	/**
	 * Extracts from the clauses array all the variables and insert the in an
	 * ArrayList
	 * 
	 * @param clauses
	 *            A bidimensional array containing all the clauses
	 * @return An ArrayList containing all the variables
	 */
	protected HashMap<Integer, Boolean> extractVariables() {
		HashMap<Integer, Boolean> variables = new HashMap<Integer, Boolean>();
		for (int i = 0; i < clauses.length; i++) {
			for (int j = 0; j < clauses[i].length; j++) {
				if (!variables.containsKey(Math.abs(clauses[i][j]))) {
					variables.put(Math.abs(clauses[i][j]), false);
				}
			}
		}
		return variables;
	}

	protected boolean isValidSolution() {

		// Travel clause by clause validating using the random solution
		for (int i = 0; i < clauses.length; i++) {
			boolean clauseValid = false;
			for (int j = 0; j < clauses[i].length; j++) {
				if ((clauses[i][j] > 0 && variables
						.get(Math.abs(clauses[i][j])))
						|| (clauses[i][j] < 0 && !variables.get(Math
								.abs(clauses[i][j])))) {
					clauseValid = true;
					break;
				}
			}
			if (!clauseValid) {
				return false;
			}
		}
		return true;
	}

	protected int clausesValid() {
		// Travel clause by clause validating using the random solution
		int clausesValid = 0;
		for (int i = 0; i < clauses.length; i++) {			
			for (int j = 0; j < clauses[i].length; j++) {
				if ((clauses[i][j] > 0 && variables
						.get(Math.abs(clauses[i][j])))
						|| (clauses[i][j] < 0 && !variables.get(Math
								.abs(clauses[i][j])))) {
					clausesValid++;
					break;
				}
			}		
		}
		return clausesValid;
	}

	protected void setRandomSolutionValues() {
		for (Map.Entry<Integer, Boolean> entry : variables.entrySet()) {
			entry.setValue(Math.random() * 100 > 50);
		}
	}

	public abstract String report();
	
	@Override
	public void run() {
		solutionFound = this.solve();
		if (!solutionFound && !stopThread) {			
			System.out
					.println("No fue posible encontrar una solución al problema de SAT");			
		} else if(solutionFound) {
			System.out.println(this.report());
		}
		solverFinished = true;
	}
}
